Metaprogramming in Lean 4
from Lean
https://github.com/leanprover-community/lean4-metaprogramming-book
Lean4はElaborationという強力なメタプログラミングの機能があり、コンパイラフロントエンド自体が大体このElaborationを使ってかかれている。この記事はその概略が書いてある ref
elaboratorというparser的な謎概念があるらしい
この事実をふまえ、Leanは証明にirreducibleとタグ付けする。ファイルを処理するとき、このタグはパーサー(より正確にはelaborator)に対して、「このタグが付いたものを展開する必要はない」というヒントとして機能する。 ref
https://lean-lang.org/lean4/doc/elaborators.html
elaborationを行う
Leanには暗黙の引数を推論するための非常に複雑なメカニズムがあり、それを使うと関数型や述語、さらには証明を推論できることを見ていく。このような「穴」または「プレースホルダー」を埋めるプロセスは、elaborationとしてよく知られている。暗黙の引数の存在により、ある式の意味を正確に確定させるための情報が不十分である状況が起こりうる。id や List.nil のような表現は、文脈によって異なる意味を持つことがあるため、polymorphic(多相的)であると言われる。ref
smalltt
wasabi (@wasabi__315)
smalltt勉強になりすぎる
"Approximate Coversion Checking"のところを参考にしたら、授業で作った型検査器がめちゃくちゃ早くなった
https://github.com/AndrasKovacs/smalltt?tab=readme-ov-file
Demo project for several techniques for high-performance elaboration with dependent types.